ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), m:, A:ecl-trans-tuple{i:l}
ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), m:, A:ecl-trans-tuple(ds; da).
add-ecl-act(A; m)  ecl-trans-tuple{i:l}(ds; da) 

latex

Definitions	t  T, x:A. B(x), A  B, P  Q, False, A, , , , ma-valtype(da; k), decl-state(ds), Knd, (x  l), ff, bor(p; q), reduce(f; k; as), b, band(p; q), (i = j), if b then t else f fi , spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), add-ecl-act(A; m), ecl-trans-tuple{i:l}(ds; da), Id, x. t(x), fpf(A; a.B(a))
Lemmas	ecl-trans-tuple wf, fpf wf, Id wf, ifthenelse wf, eq int wf, band wf, bnot wf, reduce wf, bor wf, nat plus inc, bfalse wf, nat wf, l member wf, Knd wf, decl-state wf, ma-valtype wf, bool wf, nat plus wf, le wf